I needed some of these lemmas for a recent project and thought I would add them + try to shorten other proofs using them where possible.
The main result here that is useful to me is the uniq_le_perm_eq lemma, which seems to encompass the other lemmas that are there currently, provided you also have the perm_eq_uniq_impl lemma. I know that these are derivable from the present lemmas, but this is not directly obvious (at least it wasn't to me). And I would say this is especially so since the lemma that currently comes closest to uniq_le_perm_eq, which is uniq_perm_eq_size, uses more and stronger hypotheses than necessary (see the new proof, which clears one of the hypotheses and does not much more than directly applying a lemma with weaker hypothesis).
The other, smaller lemmas on drop and behead I included have simply been annoying me in proofs (their absence, that is).